g:IMonoid, m, n:, e:|g|. (n  (m  e)) = ((n * m)  e)  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid
Definitions	t  T, x:A. B(x), False, A, A  B, i  j , P  Q, True, T, , , P & Q, P  Q, P  Q, , x f y, IMonoid
Lemmas	imon wf, nat wf, le wf, nat properties, grp car wf, true wf, squash wf, mon nat op wf, grp id wf, mon nat op zero, mon nat op unroll, mul preserves le, grp op wf, mon nat op add